|
|
Automatický theorem prover
Mazánek, Martin ; Havlena, Vojtěch (oponent) ; Lengál, Ondřej (vedoucí práce)
Tato bakalářská práce se zabývá implementací systému pro automatické dokazování vět výrokové a predikátové logiky používajícím rezoluci. Cílem této práce je vytvořit jednoduchý systém a zdokumentovat jeho vývoj, nikoliv tvorba konkurenceschopného systému. Dále je v práci představeno několik populárních systémů automatického dokazování.
|
|
|
Implementace mandátu mise UNPROFOR v Bosně a Hercegovině v letech 1992-1995
Lalić, Jan ; Tejchman, Miroslav (vedoucí práce) ; Pikal, Kamil (oponent)
Neochota mezinárodního společenství zapojit se do bosenské občanské války v letech 1992- 1995 vojenskou intervencí, vytvořila z mise United Nations Protection Force (UNPROFOR) náhražku rozhodné akce. Absence jakékoliv naděje na dohledné příměří, které by mohly mírové jednotky svojí přítomností podporovat, vedla v první fázi války k vytvoření ryze humanitárního mandátu pro jednotky OSN. Ty měly ve spolupráci s Úřadem vysokého komisaře OSN pro uprchlíky (UNHCR) zajistit chod sarajevského letiště pro humanitární účely a postarat se o bezpečnost UNHCR a jeho konvojů s humanitární pomocí. Práce "Implementace mandátu mise UNPROFOR v Bosně a Hercegovině v letech 1992-1995" se zabývá právě problematikou implementace tohoto čistě humanitárního mandátu. Pomocí deskriptivní analýzy nejdříve vysvětlí motivy, které vedly mezinárodní společenství k nasazení lehce vyzbrojených mírových jednotek s netypickým mandátem do oblasti, která se ukáže být naprosto nevhodnou pro působení mírových sil. Následně prozkoumá samotný průběh implementace a problémy, se kterými se jednotky OSN potýkaly. Cílem práce je dokázat, že mise UNPROFOR nebyla absolutním selháním, za jaké je pokládána, avšak prokáže se neadekvátnost jejího nasazení v daném prostředí a budou představeny příčiny neúspěchů.
|
|
|
Hledání minimálních splňujících ohodnocení Booleovských formulí
Švancara, Jiří ; Balyo, Tomáš (vedoucí práce) ; Trunda, Otakar (oponent)
V této práci zkoumáme algoritmy a techniky pro řešení Booleovské splnitelnosti. Dále se zabýváme možnostmi jejich použití při řešení weighted short SAT, což je zobecnění problému splnitelnosti. Toto zobecnění požaduje nalézt splňující ohodnocení za použití minimálního součtu vah proměnných. K řešení tohoto problému zavádíme tři pravdivostní ohodnocení proměnných - True, False a Unassign. Ukážeme, že ne všechny algoritmy a techniky používané v moderních SAT solverech můžeme aplikovat v našem programu. Ty, které můžeme, převedeme tak, aby používali námi nadefinované pravdivostní ohodnocení. Různou kombinací takto převedených technik dostaneme několik verzí solveru, které mezi sebou na závěr porovnáme. Powered by TCPDF (www.tcpdf.org)
|
|
|
On the Power of Weak Extensions of V0
Müller, Sebastian Peter ; Krajíček, Jan (vedoucí práce) ; Thapen, Neil (oponent) ; Kolodziejczyk, Leszek (oponent)
Název práce: O síle slabých rozšírení teorie V0 Autor: Sebastian Müller Katedra: Katedra Algebry Vedoucí disertační práce: Prof. RNDr. Jan Krajíček, DrSc., Katedra Algebry. Abstrakt: V predložené disertacní práci zkoumáme sílu slabých fragmentu arit- metiky. Činíme tak jak z modelově-teoretického pohledu, tak z pohledu důkazové složitosti. Pohled skrze teorii modelu naznačuje, že malý iniciální segment libo- volného modelu omezené aritmetiky bude modelem silnější teorie. Jako příklad ukážeme, že každý polylogaritmický řez modelu V0 je modelem VNC. Užitím známé souvislosti mezi fragmenty omezené aritmetiky a dokazatelností v ro- zličných důkazových systémech dokážeme separaci mezi rezolucí a TC0 -Frege systémem na náhodných 3CNF-formulích s jistým poměrem počtu klauzulí vůci počtu proměnných. Zkombinováním obou výsledků dostaneme slabší separační výsledek pro rezoluci a Fregeho důkazové systémy omezené hloubky. Klíčová slova: omezená aritmetika, důkazová složitost, Fregeho důkazový systém, Fregeho důkazový systém omezené hloubky, rezoluce Title: On the Power of Weak Extensions of V0 Author: Sebastian Müller Department: Department of Algebra Supervisor: Prof. RNDr. Jan Krajíček, DrSc., Department of Algebra....
|
|
|
Význam Rady bezpečnosti OSN a právní závaznost rezolucí při zajišťování mezinárodního míru a bezpečnosti
Urbanová, Petra ; Ondřej, Jan (vedoucí práce) ; Balaš, Vladimír (oponent)
- Význam Rady bezpečnosti OSN a právní závaznost rezolucí při zajišťování mezinárodního míru a bezpečnosti Tato práce pojednává o historii předcházející vzniku, a o samotném vzniku OSN a Rady bezpečnosti, na který navazuje kapitola věnující se stálým a nestálým členům Rady s podkapitolou týkající se reformních návrhů z hlediska jejího složení. Podrobně jsou zde rozebrány funkce a pravomoci Rady bezpečnosti, obsahující také pasáž týkající se období ochromení činnosti Rady. V kapitole o způsobu usnášení Rady je věnována pozornost jak zásadní problematice rozlišení otázek procedurálních a neprocedurálních, tak institutu veta. Závěrečná kapitola se věnuje rozhodnutím Rady bezpečnosti se zaměřením na rezoluce a jejich právní závaznost.
|
|
|
Automatický theorem prover
Mazánek, Martin ; Havlena, Vojtěch (oponent) ; Lengál, Ondřej (vedoucí práce)
Tato bakalářská práce se zabývá implementací systému pro automatické dokazování vět výrokové a predikátové logiky používajícím rezoluci. Cílem této práce je vytvořit jednoduchý systém a zdokumentovat jeho vývoj, nikoliv tvorba konkurenceschopného systému. Dále je v práci představeno několik populárních systémů automatického dokazování.
|
|
|
The Resolution Fund: Is behaviour of the contributing institutions affected by the applied methodology?
Hykl, Daniel ; Pečená, Magda (vedoucí práce) ; Džmuráňová, Hana (oponent)
Daniel Hykl Bakalářská práce Fond pro řešení krize: Ovlivňuje aplikovaná metodika chování přispívajících institucí? Abstrakt Bakalářská práce zkoumá v teoretické rovině způsob výpočtu ročních příspěvků do Fondu pro řešení krize, které jsou stanoveny na základě bankovních rozvah k poslednímu dni roku, a jeho vliv na banky a finanční sektor. Problém vertikálního rozdělení sektorového příspěvku mezi jednotlivé banky je demonstrován na několika teoretických příkladech. Hypotéza o optimalizaci rozvah bank ke konci roku za účelem dosažení nižšího ročního příspěvku je ověřována na základě vývoje závazků sedmi největších bank v České republice a na základě teoretických výší závazků ke konci roku spočtených pro scénář nulové optimalizace. Práce odhaduje roční příspěvky bank a porovnává je s teoretickými příspěvky spočtenými z teoretických závazků.
|
|
|
Legalita vojenského zásahu během občanské války v Jemenu
Hambálek, Jiří ; Bílková, Veronika (vedoucí práce) ; Ondřej, Jan (oponent)
Shrnutí Cílem této práce bylo odpovědět na otázku, byl-li vojenský zásah koalice vedené Saúdskou Arábií, provedený v rámci operace Decisive Storm v průběhu občanské války v Jemenu v roce 2015 v souladu s mezinárodním právem či nikoli. Za tímto účelem je práce rozdělena do tří částí. První část práce, tvořená kapitolami 1 - 6, je zaměřena na rozbor případů legálního použití síly v mezinárodních vztazích, tedy případů sebeobrany, akcí Rady bezpečnosti podle kapitoly VII Charty OSN, intervence na pozvání vlády, koncept humanitární intervence a koncept R2P a roli oblastních dohod a organizací kolektivní bezpečnosti při udržování mezinárodního míru a bezpečnosti. Druhá část, tvořená kapitolou 7, obsahuje případovou studii, jejímž předmětem je počátek občanské války v Jemenské republice na přelomu let 2014 a 2015. Tato kapitola se zabývá příčinami a průběhem politické krize, která přerostla v občanskou válku mezi hútijskými milicemi a vládními ozbrojenými silami a vyvrcholila svržením prezidenta Hádího a následnou intervencí vojenských sil koalice arabských států vedené Saúdskou Arábií, na podporu jemenské vlády. Účelem této kapitoly je poskytnout ucelený a podrobný přehled aktivit jednotlivých aktérů konfliktu, zejména politických rozhodnutí prezidenta Hádího, okolností jejich přijetí, rozbor příslušných...
|
|
|
Role mírových jednotek UNPROFOR během války v Bosně a Hercegovině se zaměřením na bezpečnou zónu Goražde
Poláková, Michaela ; Žíla, Ondřej (vedoucí práce) ; Šístek, František (oponent)
Bakalářská práce si klade za cíl analyzovat působení mírových jednotek UNPROFOR (United Nations Protection Force) během války v Bosně a Hercegovině mezi lety 1993-1995. Vyslání mírové mise bylo ze začátku konfliktu jedinou výraznější reakcí západních států ve věci jeho řešení. Žádný ze států mezinárodního společenství nebyl ochotný zapojit se do bojů přímo. Vyslání humanitární mise OSN mělo být prozatímním řešením, které mělo ulehčit strádajícímu civilnímu obyvatelstvu. Zpočátku bylo hlavním úkolem mise UNPROFOR zajistit bezpečí a chod sarajevského letiště, jež bylo hlavní tepnou pro dopravu humanitární pomoci. S postupem konfliktu byl však mandát mírových jednotek rozšiřován, například na ochranu humanitárních konvojů, jež přepravovaly materiál ze sarajevského letiště po celé BaH. Důležitým okamžikem v jednání mezinárodního společenství se stalo vytvoření bezpečných zón. Nejprve kolem Srebrenice, poté i okolo dalších pěti bosenských sídel, konkrétně Tuzly, Bihaće, Goražde, Žepy a Sarajeva. Tyto enklávy měly zajistit za pomoci UNPROFOR ochranu civilnímu obyvatelstvu a přístup k základním potřebám. Cílem této práce je nalézt konkrétní důvody poměrného neúspěchu mise UNPROFOR, a určit, zda za tímto nezdarem stály působící jednotky, či mezinárodní společenství. Projekt pracuje s hypotézou, která...
|
|
|
Legalita vojenského zásahu během občanské války v Libyi
Hambálek, Jiří ; Bílková, Veronika (vedoucí práce) ; Faix, Martin (oponent)
Shrnutí Cílem této práce bylo odpovědět na otázku, byl-li zásah NATO, provedený v rámci operace Unified Protector v průběhu občanské války v Libyi v roce 2011, v souladu s mezinárodním právem či nikoli. Za tímto účelem je práce rozdělena do tří částí. První část práce, tvořená kapitolami 1 - 5, je zaměřena na rozbor případů legálního použití síly v mezinárodních vztazích, tzn., případů sebeobrany a akcí Rady bezpečnosti podle kapitoly VII Charty OSN, značně kontroverzní koncept humanitární intervence a koncept R2P a roli oblastních dohod a organizací kolektivní bezpečnosti při udržování mezinárodního míru a bezpečnosti. Druhá část, tvořená kapitolou 6, obsahuje případovou studii, jejímž předmětem je občanská válka v Libyi v roce 2011. Tato kapitola se zabývá průběhem celého vnitrostátního konfliktu mezi libyjskou vládou, reprezentující autoritativní režim plukovníka Muammara Kaddáfího a povstalci, podporovanými vojenskými silami NATO a některými evropskými státy. Účelem této kapitoly je poskytnout ucelený a podrobný přehled jednotlivých vojenských operací obou stran konfliktu, rozbor rezolucí Rady bezpečnosti, věnovaných řešení tohoto konfliktu a dále též rozbor vojenského zásahu NATO v rámci operace Unified Protector. Třetí část této práce, reprezentovaná kapitolou 7, je věnována hodnocení legality...
|
host ::
RSS.